perm filename TAKASU.LE3[LET,JMC] blob
sn#216855 filedate 1976-05-25 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 .require "let.pub[let,jmc]" source
C00004 ENDMK
C⊗;
.require "let.pub[let,jmc]" source;
∂AIL Professor S. Takasu↓Research Institute for Mathematical Sciences
↓Kyoto University↓Kyoto, Japan∞
Dear Professor Takasu:
I was delighted to receive your letter, and the signed
agreement has been forwarded. As you will see, I couldn't resist exercising
the bureaucratic stamp I got in Kyoto. When are you visiting
Stanford, with whom, and for how long?
Enclosed is a preliminary writeup of a new idea of mine
for getting rid of both opaque contexts and quotation marks in
treating knowledge and the modalities. I have showed it to several
people here and at M.I.T., almost everyone finds the approach
promising.
Our new KL-10 processor should be working in less than a
month, and we expect a factor of five in speed from it, so there
will be plenty of computing resources for the proof checker, etc.
Bill Glassmire has completed a proof of correctness of the
McCarthy-Painter compiler in FOL, and there are numerous ideas
for improving its applicability to MTC. Also a graduate student,
Christopher Goad, has a proof that the first two wise men don't
know the colors of their spots.
We are all looking forward to your visit.
.sgn